/**
 * Software Analysis and Verification 
 * @project: Verify Pattern Matching with Guards in Scala
 * @authors: Mirco Dotta and Philippe Suter
 */


package ch.epfl.lara.patterns.utils;

import ch.epfl.lara.patterns.ast._

import FreshRenamer.{Subs}

object Substitution {

  def apply(subst: Subs, pattern: Pattern): Pattern = pattern match {
    case guardedPattern @ _ if(guardedPattern.isInstanceOf[GuardedPattern]) =>
      this(subst,guardedPattern.asInstanceOf[GuardedPattern])
    case klassPattern @ _ if(klassPattern.isInstanceOf[KlassPattern]) =>
      this(subst,klassPattern.asInstanceOf[KlassPattern])
  }
  
  def apply(subst: Subs, pattern: GuardedPattern): GuardedPattern = pattern match {
    case GuardedKlass(klass,guard) => 
      GuardedKlass(this(subst,klass),this(subst,guard))
  }
  
  def apply(subst: Subs, pattern: KlassPattern): KlassPattern = pattern match {
    
    case Klass(name,args) => 
      Klass(name,args.map(arg => this(subst,arg)))
      
    case _ => pattern
  }
  

  def apply(subst: Subs, arg: ArgPattern): ArgPattern = arg match {
    case SimpleArgument(ident,typez) => 
      SimpleArgument(substitute(subst,ident),typez)
    
    case klass @ _ if(klass.isInstanceOf[KlassPattern]) => this(subst,klass.asInstanceOf[KlassPattern])
  }
  
  
  /**
   * <p>
   * 	Apply substitution to a guard 
   * </p>
   * @param subst: The list of pair of substitutions
   * @param guard: The guard whose sensible to the substitutions
   * @return     : The new guard with the applied substitutions
   */
  def apply(subst: Subs, guard: Guard): Guard = guard match {
    case Assume(f) => Assume(this(subst,f))
  }
  
   
  /**
   * <p>
   * 	Apply substitution to a formula
   * </p>
   * @param subst: The list of pair of substitutions
   * @param guard: The formula whose sensible to the substitutions
   * @return     : The new formula with the applied substitutions
   */
  def apply(subst: Subs, formula: Formula): Formula = formula match {
   
    case Imply(left,right) => Imply(this(subst,left),this(subst,right))

    case Or(left,right) => Or(this(subst,left),this(subst,right))

    case And(left,right) => And(this(subst,left),this(subst,right))

    case Not(f) => Not(this(subst,f))

    case Forall(x,f) => Forall(this(subst,x),this(subst,f))

    case Exists(x,f) => Exists(this(subst,x),this(subst,f))

    case In(elem,set) => In(this(subst,elem),this(subst,set))

    case SubsetEq(s1,s2) => SubsetEq(this(subst,s1),this(subst,s2))

    case Equal(e1,e2) => Equal(this(subst,e1),this(subst,e2))

    case Less(e1,e2) => Less(this(subst,e1),this(subst,e2))

    case LessEq(e1,e2) => LessEq(this(subst,e1),this(subst,e2))
   
    case _ => formula
  }

   
   /**
    * <p>
    * 	Apply substitution to a term
    * </p>
    * @param subst: The list of pair of substitutions
    * @param guard: The term whose sensible to the substitutions
    * @return     : The new term with the applied substitutions
    */
  def apply(subst: Subs, term: Term): Term = term match {
    case set @ _ if set.isInstanceOf[Set] => this(subst,set.asInstanceOf[Set])
    case elem @ _ if elem.isInstanceOf[Element] => this(subst,elem.asInstanceOf[Element])
  }
    
    
  /**
   * <p>
   * 	Apply substitution to a set
   * </p>
   * @param subst: The list of pair of substitutions
   * @param guard: The set whose sensible to the substitutions
   * @return     : The new set with the applied substitutions
   */
  def apply(subst: Subs, set: Set): Set = set match {
    case VarSet(name) => VarSet(substitute(subst,name))
    case Singleton(elem) => Singleton(this(subst,elem))
  }
    

  /**
   * <p>
   * 	Apply substitution to an element
   * </p>
   * @param subst: The list of pair of substitutions
   * @param guard: The element whose sensible to the substitutions
   * @return     : The new element with the applied substitutions
   */
  def apply(subst: Subs, elem: Element): Element = elem match {
    case Var(name) => Var(substitute(subst,name))
    case FunctionCall(Var(name), param) => FunctionCall(Var(substitute(subst,name)),this(subst,param))
    case IntValue(value) => elem
  }
  
    
  /**
   * <p>
   * 	Lookup in the substitution list for a substitution that match the
   *	name gave in argument. 
   * </p>
   * @param subst: The list of pair of substitutions
   * @param name : The string name looked up for substitution
   * @return     : Either the substitution to name if it is found in the list or the old name
   */
  private def substitute(subst: Subs, name: String): String = {
    subst find (pair => pair._1 equals name) match {
      case None => name
      case Some((oldName,newName)) => newName
    }
  }
}